fix(a2ml): normative Idris2 core now type-checks (10/10 modules) - #567
Merged
Conversation
…gate SPEC.adoc §3.1 calls `src/A2ML/` normative and authoritative. Nothing built it — no .ipkg anywhere, no CI job — and it did not compile. Now 10/10 modules type-check under idris2 0.7.0, verified locally, and a real gate enforces it. No postulate, no believe_me, no assert_total. Root causes: - Data.String.strIndex is NON-COVERING in 0.7.0, so it can never appear under %default total; peek/char also pattern-matched its Char result as if it were Maybe Char. That one mistake caused 7 of the 16 unification errors. Replaced with a total, covering strIndexSafe. - Consuming loops (skipWhitespace, countHashes, parseBullets, parseBlocks) had no structural decrease; each now recurses on explicit fuel derived from the remaining input. - prettyPrint / collectIds / collectRefs recursed via `MkDoc s.body`. A record projection is not structural descent to the termination checker; matching the MkSec constructor and recursing on List Block makes the decrease visible. - `<|>` was declared inside a where block, where it does not resolve. Replaced with a top-level `orElse`. - collectIds/collectRefs were private AND partial, so parseAndValidate could not use them. Now total and exported. - A2ML.Proofs did not compile at all: `All` used without importing Data.List.Quantifiers; `elemAppend` referenced twice but defined nowhere (replaced by elemAppendLeft/elemAppendSplit, each proved by induction on the Elem witness); `|>` is not an Idris2 operator; and two proofs referenced their own argument before binding it while projecting fields shared by three records. - ParserTests tested an API that does not exist (parse, uniqueIdsDec, refsResolveDec, hasAbstractDec). Rewritten against the real API — which uncovered a genuine gap: Surface.SDoc and Translator.translate exist, but NOTHING produces an SDoc. There is no surface parser. - Added Eq Id, delegating to the existing idEq. The CI gate could NOT be included here: this token lacks GitHub's `workflow` scope, so it cannot create `.github/workflows/`. The workflow is drafted and posted on #556 for the owner to add — it is a real gate (no continue-on-error, no skip-if-absent) and uses the ipkg target because per-file `idris2 --check` exits 0 when an import is missing. A2ML.Converters is deliberately excluded and tracked: its renderers are mutually recursive with their own where-block helpers and need a hand-done restructure. Including it would make the gate red on arrival. Refs #556 Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review ✅ ApprovedFixes 16 type-checking errors across the normative Idris2 core modules, ensuring all 10 modules now compile cleanly under Idris2 0.7.0. No issues found.
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Important Your trial ends in 7 days — upgrade now to keep code review, CI analysis, auto-apply, custom automations, and more. Was this helpful? React with 👍 / 👎 | Gitar |
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Completes #556. The normative Idris2 core now type-checks — 10/10 modules, verified locally against idris2 0.7.0.
SPEC.adoc§3.1 callssrc/A2ML/"normative … the source files are authoritative." Nothing built it (no.ipkganywhere, no CI job) and it did not compile. Since all three dialects must agree through this core, and it's about to be registered with IANA, this is the foundation.Root causes fixed — no
postulate, nobelieve_me, noassert_totalOne mistake caused 7 of the 16 errors:
Data.String.strIndexis non-covering in Idris2 0.7.0, so it can never appear under%default total— andpeek/charpattern-matched itsCharresult as if it wereMaybe Char. Replaced with a total, coveringstrIndexSafe.skipWhitespace,countHashes,parseBullets,parseBlocks) had no structural decreaseprettyPrint/collectIds/collectRefsrecursed viaMkDoc s.bodyMkSecand recurse onList Blockdeclared inside awhere` block (doesn't resolve there)collectIds/collectRefswere private AND partialA2ML.Proofsdidn't compile at allAllused withoutData.List.Quantifiers;elemAppendreferenced twice but defined nowhere → replaced withelemAppendLeft/elemAppendSplit, each proved by induction on theElemwitness;|>isn't an Idris2 operator; two proofs referenced their own argument before binding it while projecting fields shared by three recordsParserTeststested a nonexistent API (parse,uniqueIdsDec,refsResolveDec,hasAbstractDec)Eq Id, so tests couldn't compare idsidEqA real gap this uncovered
A2ML.Surface.SDocandA2ML.Translator.translate : SDoc -> Docboth exist — but nothing produces anSDoc. There is no surface parser, so that half of the pipeline is unreachable. Worth its own issue; it matters for the dialect-factory design.Two things deliberately left out
workflowscope, so it cannot create.github/workflows/. The workflow is drafted and posted on A2ML normative Idris2 core: A2ML.Parser does not type-check (16 errors) — blocks the core CI gate #556 for you to add. It's a real gate: nocontinue-on-error, no skip-if-absent, and it uses the ipkg target because per-fileidris2 --checkexits 0 on a missing module (a fake gate).A2ML.Convertersis excluded from the package and tracked. Its renderers (toMarkdown/toDjot/toHtml/toLatex) are mutually recursive with their ownwhere-block helpers, which can't be total in that shape and needs a hand-done restructure. Including it would make the gate red on arrival. The.ipkgdocuments this scope explicitly.Verification:
cd a2ml && idris2 --typecheck a2ml-core.ipkg→ exit 0, 10/10 modules.